形式手法とは、ソフトウェアの機能仕様を数学的に記述し、開発されたプログラムがその仕様を満足することの証明も可能とすることを言う [Abrial, 2010]。機能仕様は、VDLと呼ばれるプログラミング言語に似た特殊な言語、数学的な記法に似た方法を採用するZと呼ばれる言語などで記述される。車載組込みソフトウェアの開発で自動車の安全性に悪影響を与えないことを証明する方法として、ISO26262ではそのような形式手法を応用して車載組込みソフトウェアの設計を実施することを推奨している。

Abrial U. & Glaesser, J-R編. Rigorous Methods for Software Construction and Analysis. Springer(2010).